(*************************************************************************)
(** Simply-typed Scalina  in Coq.    Definitions                         *)
(** Author: Adriaan Moors, 2008                                          *)
(*************************************************************************)

Set Implicit Arguments.
Require Import Metatheory support.
Require Import List.


(** Based on the Coq tutorial at POPL 2008, see
    "Engineering Formal Metatheory", Aydemir, Charguéraud, Pierce,
    Pollack, Weirich. POPL 2008.

    Tutorial authors: Brian Aydemir and Stephanie Weirich, with help
    from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey
    Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic.  Adapted from
    code by Arthur Charguéraud.
*)

(*************************************************************************)


(*************************************************************************)
(** * Syntax of Simply Typed Scalina *)
(*********************************************************************)
 
(*
Inductive level : Set := terms | types | kinds.
Inductive lab   : level -> Set
Inductive classified : level -> Set
  | cls_tm : option tm -> tp -> classified terms
  | cls_tp : option tp -> kd -> classified types.5
Inductive mem (L: level)  :  Set = 
  | m : lab L -> classified L -> mem L.
*)

Inductive lab : Set :=
  | ltm  : nat -> lab.  (* term label *)
(*  | ltp  : nat -> lab.  (* type label *) *)

Inductive tp : Set :=
  | tp_single : tm -> tp
  | tp_struct : option tp -> list mem  -> tp (* self type, list of members *)

(* due to recursive structure, using a set to hold the members is too 
complicated -- this is more faithful to distinction between syntax and 
well-formedness anyway*)

with mem : Set :=
  | mtm : lab -> tp -> option tm -> mem

with tm : Set :=
  | bvar : nat  -> tm    (* bound variables *)
  | fvar : var -> tm   (* free  variables *)
  | sel  : tm -> lab  -> tm
  | new  : tp  -> tm.

(* better not to integrate `stable` into `tp_single`: turn this into a kind of pluggable type annotation later?
integrate with linear types/effect system
*)
Inductive stable : tm -> Prop :=
  | stable_bvar : forall n, stable (bvar n)
  | stable_fvar : forall v, stable (fvar v)
  | stable_sel : forall t l, stable t -> stable (sel t l)
  | stable_obj : forall T, stable (new T).
 
Hint Constructors stable.

Coercion bvar : nat >-> tm.
Coercion fvar : var >-> tm.

Function lab_getIdx (l: lab) {struct l} : nat :=
  match l with
  | ltm n => n
(*  | ltp n => n*)
  end.

Function mem_getLabel (m: mem) {struct m} : lab :=
  match m with
  | mtm l _ _ => l
  end.

Function mem_getRhs (m: mem) {struct m} : option tm :=
  match m with
  | mtm _ _ o => o
  end.

Function mem_getClassifier (m: mem) {struct m} : tp :=
  match m with
  | mtm l t _ => t
  end.

Require Import OrderedType OrderedTypeEx.

Module Import Nat_as_OT_Facts := OrderedTypeFacts Nat_as_OT.

Lemma eq_lab_dec : forall x y : lab, { x = y } + { x <> y }.
Proof.
  decide equality.
  decide equality.
Qed.

Function mems_lookup  (l: lab) (ms: list mem)  {struct ms} : option mem :=
  match ms with
  | nil => None
  | m' :: E' => if eq_lab_dec l (mem_getLabel m') then (Some m') else mems_lookup l E'
  end.


Notation "mems ?: l " := (option_map mem_getClassifier (mems_lookup l mems)) (at level 67).


(*************************************************************************)
(** * Opening *)
(*************************************************************************)

(** Opening replaces an index with a term. It corresponds to informal
    substitution for a bound variable, such as in the rule for beta
    reduction. Note that only "dangling" indices (those that do not
    refer to any abstraction) can be opened. Opening has no effect for
    terms that are locally closed.

    Natural numbers are just an inductive datatype with two
    constructors: O and S, defined in Coq.Init.Datatypes.
    The notation [k === i] is the decidable equality function for
    natural numbers (cf. Coq.Peano_dec.eq_nat_dec).
    This notation is defined in the [Metatheory] library.

    We make several simplifying assumptions in defining [open_rec].

    First, we assume that the argument [u] is locally closed.  This
    assumption simplifies the implementation since we do not need to
    shift indices in [u] when passing under a binder.  Second, we
    assume that this function is initially called with index zero and
    that zero is the only unbound index in the term.  This eliminates
    the need to possibly subtract one in the case of indices.

    There is no need to worry about variable capture because bound
    variables are indices.
*)

Fixpoint open_rec_tm (k : nat) (u : tm) (e : tm) {struct e} : tm :=
  match e with
    | bvar i => if k === i then u else (bvar i)
    | fvar x => fvar x
    | sel e1 l => sel (open_rec_tm k u e1) l
    | new T => new (open_rec_tp k u T)
  end
with open_rec_tp (k : nat) (u : tm) (t : tp) {struct t} : tp :=
  match t with
    | tp_single p => tp_single (open_rec_tm k u p)
    | tp_struct self mems => tp_struct (option_map (open_rec_tp k u) self) 
           (List.map (open_rec_mem (k+1)(* go under binder (the self variable) *) u) mems)
  end
with open_rec_mem (k : nat) (u : tm) (m : mem) {struct m} : mem :=
  match m with
    | mtm l T rhs => mtm l (open_rec_tp k u T)  (option_map (open_rec_tm k u) rhs)
  end.

(** We also define a notation for [open_rec].
*)

Notation "{ k ~> u } t" := (open_rec_tm k u t) (at level 67).
Notation "{ k ~tp> u } t" := (open_rec_tp k u t) (at level 67).
Notation "{ k ~mem> u } m" := (open_rec_mem k u m) (at level 67).
Definition open_rec_mems k u ms := map (open_rec_mem k u) ms. 
Notation "{ k ~mems> u } ms" := (open_rec_mems k u ms) (at level 67).

(** Many common applications of opening replace index zero with an
    expression or variable.  The following definition provides a
    convenient shorthand for such uses.  Note that the order of
    arguments is switched relative to the definition above.  For
    example, [(open e x)] can be read as "substitute the variable [x]
    for index [0] in [e]" and "open [e] with the variable [x]."
    Recall that the coercions above let us write [x] in place of
    [(fvar x)].
*)

Definition open e u := open_rec_tm 0 u e.
Definition open_tp e u := open_rec_tp 0 u e.
Definition open_mem e u := open_rec_mem 0 u e.
Definition open_mems ms u := map (open_rec_mem 0 u) ms.


Notation "t ^^ u" := (open t u) (at level 67).
Notation "t ^ x" := (open t (fvar x)).


(*************************************************************************)
(** * Local closure *)
(*************************************************************************)

(** Recall that [tm, tp, mem] admit terms that contain unbound indices. 
    We say that a term is locally closed, 
    when no indices appearing in it are unbound.  The proposition 
    [lc e] holds when an expression [e] is locally closed.

    The inductive definition below formalizes local closure such that
    the resulting induction principle serves as the structural
    induction principle over (locally closed) expressions.  In
    particular, unlike induction for type exp, there is no case
    for bound variables.  Thus, the induction principle corresponds more
    closely to informal practice than the one arising from the
    definition of pre-terms.
*)

(* for red_regular to be implied by the side condition `value (new T)` in red_sel,
`lc_tp T` must ensure that all the members in T (according to run-time expansion) are
locally closed. *)
Inductive  lc_tp : tp -> Prop :=
  | lc_single : forall p, 
      lc_tm p -> 
      lc_tp (tp_single p)
  | lc_struct_noself : forall L mems,
      (forall x:var, x \notin L -> lc_mems (List.map (open_rec_mem 0 x) mems)) ->
      lc_tp (tp_struct None mems)
  | lc_struct_self : forall L self mems,
      lc_tp self ->
      (forall x:var, x \notin L -> lc_mems (List.map (open_rec_mem 0 x) mems)) ->
      lc_tp (tp_struct (Some self) mems)
with lc_mem : mem -> Prop :=
  | lc_mtm_norhs : forall l t,
      lc_tp t ->
      lc_mem (mtm l t None)
  | lc_mtm_rhs : forall l t rhs,
      lc_tp t ->
      lc_tm rhs ->
      lc_mem (mtm l t (Some rhs))
with lc_tm : tm -> Prop :=
  | lc_var : forall x,
      lc_tm (fvar x)
  | lc_sel : forall tgt l,
      lc_tm tgt ->
      lc_tm (sel tgt l)
  | lc_new : forall t,
      lc_tp t ->
      lc_tm (new t)
with lc_mems : list mem -> Prop :=
  | lc_nil :
      lc_mems (nil)
  | lc_cons : forall m ms,
      lc_mem m -> lc_mems ms -> lc_mems (m :: ms).
(*
Inductive  lc_tp : tp -> Prop :=
  | lc_struct : forall L self mems,
      option_forAll (option_map lc_tp self) ->
      (forall x:var, x \notin L -> list_forAll (List.map (fun m => lc_mem (open_rec_mem 0 x m)) mems)) ->
      lc_tp (tp_struct self mems)
with lc_mem : mem -> Prop :=
  | lc_mtm : forall l t rhs,
      lc_tp t ->
      option_forAll (option_map lc_tm rhs) ->
      lc_mem (mtm l t rhs)
with lc_tm : tm -> Prop :=
  | lc_var : forall x,
      lc_tm (fvar x)
  | lc_sel : forall tgt l,
      lc_tm tgt ->
      lc_tm (sel tgt l)
  | lc_new : forall t,
      lc_tp t ->
      lc_tm (new t).
*)




(*************************************************************************)
(** * Free variables *)
(*************************************************************************)

(** The function [fv], defined below, calculates the set of free
    variables in an expression.  Because we are using locally nameless
    representation, where bound variables are represented as indices,
    any name we see is a free variable of a term.  In particular, this
    makes the [abs] case simple.
*)


Fixpoint fv_tm (e : tm) {struct e} : vars :=
  match e with
    | bvar i => {}
    | fvar x => {{x}}
    | sel e1 l => fv_tm e1
    | new T => fv_tp T
  end

with fv_tp (e : tp) {struct e} : vars :=
  match e with
    | tp_single p => fv_tm p
    | tp_struct self mems => (option_fold fv_tp {} self) \u (fold_left (fun (ats: vars) (m :  mem) => ats \u (fv_mem m)) mems {})
  end

with fv_mem (e : mem) {struct e} : vars :=
  match e with
    | mtm l T rhs => (fv_tp T) \u (option_fold fv_tm {} rhs)
  end.

Definition fv_mems (mems: list mem) := (fold_left (fun (ats: vars) (m :  mem) => ats \u (fv_mem m)) mems {}).



Definition env := Env.env tp.


Inductive concrete_mem : mem -> Prop :=
  | concrete_mem_tm: forall l T rhs,
      lc_tm rhs -> (*TODO: necessary? --> regularity of kinding *)
      concrete_mem (mtm l T (Some rhs)).



Reserved Notation "E |= T ~::Concrete" (at level 69). (* fake kinding for now *)
Reserved Notation "E |= T ~< R"  (at level 69).

Reserved Notation "E |= t ~: T" (at level 69).
Reserved Notation "E |= T ~::Struct" (at level 69). (* fake kinding for now *)
Reserved Notation "E |= m ~:::wf" (at level 69).
Reserved Notation "E |= m ~:::wfs" (at level 69).


(*Inductive kinding : env -> tp -> kd -> Prop :=
  | kinding_struct : forall E,
      
where "E |= T ~:: K" := (kinding E T K).*)




(*
can we do strict type *checking* (i.e., no inference)?
consider typing a member selection:
  - we need to derive a structural type for the target
     - must specify a self type for this struct
     - must specify the exact member that should be contained 
  - but:
     -  - we have no way of knowing the self type,
        - we cannot subsume the self type away, as then subsumption would not preserve well-typedness
   - (the member part is not a real problem: can subsume a concrete member to an abstract one, and 
        a more specific declared type to the expected type)

mmmh... so what? the unknown stuff is simply quantified universally and the conclusion of the typing rule
need only hold if all its premisses do...
*)

Definition MemIn (m: mem) (ms: list mem) := (In (mem_getLabel m) (map mem_getLabel ms)).

Inductive typing : env -> tm -> tp -> Prop :=
  | typing_var : forall E x T,
      wf_env E ->
      lc_tp T -> (* for typing_regular *)
      binds x T E ->
      E |= (fvar x) ~: T

   | typing_sel : forall E tgt o mems l T,
      E |= tgt ~: (tp_struct o mems)  ->  
      option_has T (mems ?: l) ->
      lc_tp T -> (* same check as below, but more elegant (easier to prove subst_typing this way)*)
(*      (forall t: tm, {0 ~tp> t} T = T) -> (* check that T did not depend on the self variable 
        -- discovered that I forgot this condition while trying to prove typing_regular *)*)
      E |= (sel tgt l) ~: T

   | typing_sel_single : forall E tgt o mems l T,
      E |= tgt ~: (tp_struct o mems)  ->  
      option_has T (mems ?: l) ->
      stable tgt ->
      E |= (sel tgt l) ~: {0 ~tp> tgt}T

   | typing_single : forall E p T,
      E |= p ~: T  ->  
      stable p ->
      E |= p ~: (tp_single p)

   | typing_new : forall E T R ms,
      (forall p, T <> tp_single p) ->
      E |= T ~< R  ->  
			R = (tp_struct None ms) -> (* don't do self-types for now *)
(*      R = (tp_struct (Some S) ms) -> E |= T ~<: S *)
      E |= R ~::Concrete ->
      E |= R ~::Struct ->
      E |= (new T) ~: T

where "E |= t ~: T" := (typing E t T)

(* TODO merge wf_tp & concrete_tp into the kinding relation *)
with wf_tp : env -> tp -> Prop :=
  | wf_single : forall E p T o ms,
      E |= p ~: T ->
      wf_tp E T ->
      E |= T ~< (tp_struct o ms) ->
      wf_tp E (tp_single p)

  | wf_struct_self : forall L E SelfTp ms,
      (forall x, x \notin L -> 
        (*list_forAll (List.map (fun m => *)
           (E & x ~ SelfTp) |= (open_mems ms x) ~:::wfs
        (*) ms)*)) ->
      lc_tp SelfTp -> (* needed for typing_regular *)
      wf_tp E SelfTp -> (* needed for typing_fresh --> TODO: does this subsume the above condition? *)
      wf_tp E (tp_struct (Some SelfTp) ms)

  | wf_struct_noself : forall E ms,
      wf_tp E (tp_struct (Some (tp_struct None ms)) ms) ->
      wf_tp E (tp_struct None ms)

where "E |= T ~::Struct" := (wf_tp E T)

(*
checks that type is instantiatable
for now, don't support explicit self types, as we don't have any relations on types yet (subtyping, normalisation, equality), 
which makes self types pretty useless
*)
with concrete_tp : env -> tp -> Prop :=
  | concrete_struct : forall E ms,
      wf_env E -> (*TODO: necessary? --> regularity of kinding *)
      lc_tp (tp_struct None ms) ->
      list_forAll (List.map concrete_mem ms)  ->
      concrete_tp E (tp_struct None ms)
where "E |= T ~::Concrete" := (concrete_tp E T)

with expand : env -> tp -> tp -> Prop :=
  | expand_struct : forall E o ms,
      wf_env E ->   (*TODO: necessary? --> regularity of kinding *)
			lc_tp (tp_struct o ms) ->
      expand E (tp_struct o ms) (tp_struct o ms) (*TODO: check that self type and members are locally closed *)

  | expand_single : forall E p T R,
      E |= p ~: T ->
(*      (forall p', ~(T = (tp_single p'))) -> *)
      E |= T ~< R ->
      expand E (tp_single p) R

where "E |= T ~< R" := (expand E T R)


with wf_env : env -> Prop :=
  | wf_env_nil : wf_env empty
  | wf_env_cons : forall E x U,
     wf_env E ->
     x # E -> 
     (forall x, x # E -> x \notin fv_tp U) -> 
     wf_env (E & x ~ U)

(*  this leads to an induction principle that's too weak when
 there is no RHS, but the proposition we're proving inductively 
does not depend on the RHS:
   (option_has rhs optRhs -> E |= rhs ~: T) ->
*) 
with wf_mem : env -> mem -> Prop :=
  | wf_mem_mtm_rhs: forall rhs E T l,
     E |= rhs ~: T ->
     wf_mem E (mtm l T (Some rhs))

  | wf_mem_mtm_norhs: forall E T l,
     wf_env E -> (* we don't induct here, so need to make sure we don't invent an invalid E *)
     lc_tp T -> (* ditto *)
     wf_tp E T -> (* ditto (typing_fresh) *)
     wf_mem E (mtm l T None)

where "E |= m ~:::wf"    := (wf_mem E m)

with wf_mems : env -> list mem -> Prop :=
  | wf_nil : forall E,
      wf_env E -> (* don't induct, so need to make sure we don't invent an invalid E *)
      wf_mems E (nil)
  | wf_cons : forall E m ms,
      wf_mem E m -> 
      ~(MemIn m ms) ->
      wf_mems E ms -> 
      wf_mems E (m :: ms)

where "E |= m ~:::wfs"    := (wf_mems E m).

Inductive value : tm -> Prop :=
  | value_new : forall T,
      (lc_tm (new T)) -> value (new T).

Inductive rt_expand: tp -> list mem -> Prop :=
  | rt_expand_struct : forall o ms,
      rt_expand (tp_struct o ms) ms.


Reserved Notation "a ~=> b" (at level 67).

Inductive red : tm -> tm -> Prop :=
  | red_sel : forall T l ms rhs,
      value (new T) -> (* for red_regular *)
      rt_expand T ms ->   (*T ~. l |-> m ->*)
      option_has rhs (option_bind mem_getRhs (mems_lookup l ms)) ->
      (sel (new T) l) ~=> (rhs ^^ (new T))

  | red_sel_tgt : forall tgt tgt' l,
      tgt ~=> tgt' ->
      (sel tgt l) ~=> (sel tgt' l)

where "a ~=> b" := (red a b).


Definition preservation := forall E t t' T,
  E |= t ~: T ->
  t ~=> t' ->
  E |= t' ~: T.

Definition progress := forall t T, 
  empty |= t ~: T ->
     value t 
  \/ exists t', t ~=> t'.

(*
*** Local Variables: ***
*** coq-prog-args: ("-emacs-U"  "-I" "../lib" "-I" "../metatheory") ***
*** End: ***
*)